E:Type, pred?:(E(E+Unit)).
SWellFounded(first(y) & x = pred(y)  E)
 (e, e':E. (e'  eventlist(pred?;e))  (e' ((x,y. first(y) & x = pred(y)  E)^*) e)) 

latex

Definitions	as @ bs, P  Q, False, x:A. B(x), P  Q, P & Q, , b, x. t(x), {T}, P  Q, (x  l), eventlist(pred?;e), x f y, R^*, Prop, WellFnd{i}(A;x,y.R(x;y)), Unit, SWellFounded(R(x;y)), x,y. t(x;y), A & B, A, b, first(e), t  T, pred(e), P  Q, x:A. B(x)
Lemmas	pred wf, first wf, assert wf, not wf, strongwellfounded wf, unit wf, strongwf-implies, rel star wf, eventlist wf, l member wf, iff wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, rel star iff, iff functionality wrt iff, member singleton, append wf, or functionality wrt iff, member append